Nuprl Lemma : finite-type_wf
0,22
postcript
pdf
T
:Type. finite-type(
T
)
Type
latex
Definitions
finite-type(
T
)
,
x
:
A
.
B
(
x
)
,
,
Surj(
A
;
B
;
f
)
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
surject
wf
,
int
seg
wf
,
nat
wf
origin
T:Type. finite-type(T) 
Type T:Type. finite-type(T) Type 
x:A. B(x)
}x:A. B(x) T